跳转至

文章背景与核心概要

当前应用于数学领域的AI系统在验证正确性（correctness）方面表现卓越，但它们却无法验证新颖性（novelty）。AI生成的定理即使能够在Lean中零错误地成功编译，也可能仅仅代表了一个先前早已确立的数学结果。

本文介绍了 AViD Journal，这是一个全新的处理流程管道，能够摄取LaTeX文章、将其数学陈述在 Lean 4 中进行形式化，并给出最终的新颖性裁决。该决策框架涵盖三个核心维度：1. 先前存在性（Prior Existence）：检查形式化文集（如 Mathlib）以及非正式数据库（利用配备时间过滤和大模型裁判的 TheoremSearch 和 Matlas）。2. 非平凡性（Non-Triviality）：使用自动化策略评估陈述。3. 结构距离（Structural Distance）：通过前提集的杰卡德距离（Jaccard distance）来衡量证明的新颖性。

当在因声明重复而被arXiv撤回的论文上进行评估时，该管道得出了比单纯标准性能指标更深层次的定性见解，揭示了三大根本性的系统障碍： 语义保真度（Semantic Fidelity）：Lean文件的成功编译并不能本征保证对原始非正式文本的语义保真度。 召回率上限（Recall Ceiling）：召回率的极限受限于定理索引的覆盖范围，而非所选的相似性度量。 复现挑战（Reproducibility Challenges）*：arXiv通常会在撤回论文时删除源代码，这给基准测试的复现带来了困难。

Beyond Correctness: Toward Automated Novelty Verification with Lean 4

Current artificial intelligence systems applied to mathematics excel at verifying correctness, but they fail to verify novelty. An AI-generated theorem can compile successfully in Lean without errors while still representing a previously established result.

Metadata Details
arXiv ID 2608.14669
Primary Subject Computer Science > Artificial Intelligence (cs.AI)
Authors Ayrton Porto
Submitted August 2, 2026
Comments 20 pages. Preliminary version. Code available on GitHub.
Classifications MSC: 68V15, 68V20, 68T05
ACM: I.2.3; F.4.1
Metadata Details
arXiv ID 2608.14669
Primary Subject Computer Science > Artificial Intelligence (cs.AI)
Authors Ayrton Porto
Submitted August 2, 2026
Comments 20 pages. Preliminary version. Code available on GitHub.
Classifications MSC: 68V15, 68V20, 68T05
ACM: I.2.3; F.4.1

Summary

Summary

本文介绍了 AViD Journal，这是一个全新的处理流程管道，能够摄取LaTeX文章、将其数学陈述在 Lean 4 中进行形式化，并给出最终的新颖性裁决。该决策框架涵盖三个核心维度： 1. 先前存在性：检查形式化文集（如 Mathlib）以及非正式数据库（利用配备时间过滤和大模型裁判的 TheoremSearch 和 Matlas）。 2. 非平凡性：使用自动化策略评估陈述。 3. 结构距离：通过前提集的杰卡德距离来衡量证明的新颖性。

This paper introduces AViD Journal, a novel pipeline that ingests a LaTeX article, formalizes its mathematical statements in Lean 4, and issues a definitive novelty verdict. The decision framework operates across three core dimensions: 1. Prior Existence: Checks formal corpora (such as Mathlib) and informal databases (using TheoremSearch and Matlas equipped with temporal filtering and an LLM judge). 2. Non-Triviality: Evaluates the statements using automatic tactics. 3. Structural Distance: Measures proof novelty via the Jaccard distance over premise sets.

当在因声明重复而被arXiv撤回的论文上进行评估时，该管道得出了比单纯标准性能指标更深层次的定性见解，揭示了三大根本性的系统障碍： * 语义保真度：Lean文件的成功编译并不能本征保证对原始非正式文本的语义保真度。 * 召回率上限：召回率的极限受限于定理索引的覆盖范围，而非所选的相似性度量。 * 复现挑战：arXiv通常会在撤回论文时删除源代码，这给基准测试的复现带来了困难。

When evaluated on papers withdrawn from arXiv due to declared duplication, the pipeline yielded deeper qualitative insights than standard performance metrics alone, uncovering three fundamental systemic obstacles: * Semantic Fidelity: Successful compilation of a Lean file does not inherently guarantee semantic fidelity to the original informal text. * Recall Ceiling: The limit on recall is bound by the coverage of theorem indices rather than the chosen similarity metric. * Reproducibility Challenges: arXiv routinely removes source code upon paper withdrawal, complicating benchmark replication.